Inference at * 1 1 
Iof proof for Lemma fseg transitivity:



1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. L1 : T List
6. l2 = (L1 @ l1)
7. L : T List
8. l3 = (L @ l2)
  (L @ L1 @ l1) = ((L @ L1) @ l1) 

latex

 by InteriorProof ((RWO "append_assoc" 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	as @ bs, P  Q, P & Q, x:A  B(x), type List, x:A. B(x), s = t, P  Q, P  Q, x:AB(x)
Lemmas	iff wf, rev implies wf, append assoc